es:event_system{i:l}, T:Type, c:T, i,x:Id.
init-p(es; i; T; x; c)
 guard((es-dtype(es; i; x; T)
 guard(c alle-at(es; i; e.((es-first(es; e))  (es-when(es; x; e) = c  T))))) 

latex

Definitions	sq_type(T), P  Q, prop{i:l}, t  T, alle-at(es; i; e.P(e)), es-dtype(es; i; x; T), A c B, guard(T), init-p(es; i; T; x; v), P  Q, x:A. B(x), P  Q
Lemmas	Id sq, event system wf, es-isconst wf, es-E wf, es-loc wf, Id wf, es-first wf, assert wf, es-vartype wf, es-initially wf, es-dtype wf, es-when-first-discrete